i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, v:T, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
x  dom(ds)
 (A:Realizer.
 (R-Feasible(A)
 ( R-occurs(A;i;x)
 ( ds || R-ds(A;i)
 ( da || R-da(A;i)
 ( (kks. isrcv(k)  R-da(A;source(lnk(k)))(k)?Void  Valtype(da;k))
 ( (kks. k  dom(da))
 ( (k:Knd. (k  ks)  write-restricted(A;i;k))
 ( (y:Id. y  dom(ds  x : T)  read-restricted(A; i; y))
 ( R-state-var-init(i;ds;da;x;T;v;ks;tr) || A) 

latex

Definitions

t  T, P  Q, x:A. B(x), @loc x initially v:T, A || B, R-state-var(i;ds;da;x;T;ks;tr), P & Q, Void, x:A. B(x), Top, R-state-var-init(i;ds;da;x;T;v;ks;tr), Id, Type, x. t(x), a:A fp B(a), Knd, type List, x:AB(x), Valtype(da;k), State(ds), (x  l), {x:A| B(x) }, x.A(x), IdDeq, x  dom(f), b, A, Realizer, R-Feasible(R), R-occurs(R;i;z), R-ds(R;i), f || g, R-da(R;i), KindDeq, lnk(k), source(l), f(x)?z, isrcv(k), Prop, xL. P(x), write-restricted(R;i;k), read-restricted(R; i; y), x : v, f  g

Lemmas

fpf-join wf, fpf-single wf, top wf, read-restricted wf, write-restricted wf, l all wf, isrcv wf, subtype rel wf, fpf-cap wf, lsrc wf, lnk wf, Kind-deq wf, R-da wf, fpf-compatible wf, R-ds wf, R-occurs wf, R-Feasible wf, es realizer wf, not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, l member wf, decl-state wf, ma-valtype wf, Knd wf, fpf wf, Id wf, R-compat-Rplus-sq, R-state-var-compat, not-R-occurs-init-compat